Commentary by Chris Pressey
===========================

<!--
Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.

SPDX-License-Identifier: CC-BY-ND-4.0
-->

This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
exception: the ratings may be freely used for any purpose with no limitations.

TLA+
----

### The Temporal Logic of Actions

*   rating: classic

I'm doing myself a disservice by not glossing this in full.

TLA+ is reasonably well known but this paper itself is seemingly little-known.

TLA is a temporal logic, but it is also a dynamic logic ("action logic"; logic of
sequential progression of states).  It seems to be a "good" combination of these
two approaches, in that its combination does not annul the benefits of either
of the individual component logics.

There is more detail to it than this: the Wikipedia article on dynamic logic
has a section about "endogenous" vs "exogenous" logic; endogenous logics (such as
temporal logic) are more abstract in some sense, and so better equipped to
deal with questions of concurrent behaviour.

The TLA combination seems to combine the two into (an endogenous?) single logic
without losing that capacity to deal effectively with concurrency.

This is possibly due to the so-called "stuttering" - handling of what are basically
an unbounded set of null transitions between real transitions - which is apparently
critical to use TLA effectively, and I can kind of see why.

Another thing is that it's not just a logic, it's also a synax *for* logic (the
indented groups of conjunctions and disjunctions).  I have to wonder how much this
has dampened its adoption.

### The TLA+ Home Page

*   rating: 1

.

### Learn TLA+ --- Learn TLA+

*   rating: 1

.

### Practical TLA+ by Hillel Wayne

*   rating: 1

.

### tlaplus/PlusPy: Python interpreter for TLA+ specifications

*   rating: 2

Most TLA+ tools do model checking or theorem proving, but this one is actually an interpreter.